ABS: if a=1 b then x else y

ABS: '$x'1

ABS: '$x'2

STM: atom1 sq

STM: atom2 sq

ABS: AtomFree(T;x)

STM: atom-free wf

STM: atom-free-level-subtype

STM: sq stable atom-free

STM: atom-free-function

STM: atom-free-dep-function

STM: atom-free-union

STM: atom-free-settype

STM: atom-free-atom

STM: atom-free-atom2

STM: atom-free-nat

STM: atom-free-int

STM: atom-free-list

ABS: eq_atom$n(x;y)

STM: eq atom wf1

STM: eq atom wf2

STM: decidable atom equal 1

STM: decidable atom equal 2

STM: assert of eq atom1

STM: assert of eq atom2

STM: neg assert of eq atom1

STM: atom-test1

ABS: M(a;g;x)

STM: matters wf

ABS: x:T>>a

STM: inheres wf

STM: inherence-ap-elim

STM: inherence-trivial

STM: atom-inherence

STM: pair-inherence

STM: inl-inherence

STM: inr-inherence

STM: outl-inherence

STM: subtype-inherence

STM: settype-inherence

STM: top-inherence

STM: nat-inherence

ABS: |x|

STM: abs-val wf

STM: int-inherence

STM: list-inherence